es:ES, e':E, P:({e:E| loc(e) = loc(e')  Id} ). e@loc(e'). Dec(P(e))  Dec(e<e'. P(e)) 

latex

Definitions	x:A. B(x), , P  Q, x(s), t  T, x. t(x), P & Q, A c B, b, tt, if b then t else f fi , ff, Dec(P), True, P  Q, e@i. P(e), WellFnd{i}(A;x,y.R(x;y)), {T}, P  Q, P  Q, , Unit, A, False,
Lemmas	es-locl-wellfnd, event system-level-subtype, Id wf, es-loc wf, alle-at wf, decidable wf, alle-lt wf, es-E wf, es-locl wf, subtype rel self, event system wf, decidable functionality, es-pred wf, es-loc-pred, alle-lt-iff, bool wf, eqtt to assert, iff transitivity, assert wf, bnot wf, not wf, eqff to assert, assert of bnot, true wf, es-pred-locl, subtype rel function